es:event_system{i:l}, x,i:Id, T:Type.
(x,y:T. decidable((x = y  T)))
 es-dtype(es; i; x; T)
 (e',e:es-E(es).
 es-le(es; e; e')
  (loc(e') = i)
  ((es-after(es; x; e') = es-when(es; x; e)  T))
  (ev:es-E(es)
  (((es-le(es; e; ev)  es-le(es; ev; e'))
  ( ((es-after(es; x; ev) = es-when(es; x; ev)  T))))) 

latex

Definitions

x:A. B(x), P  Q, t  T, prop{i:l}, x. t(x), subtype(S; T), x:A. B(x), P  Q, A c B, P  Q, P  Q, sq_type(T), guard(T), T, True, l_exists(L; T; x.P(x)), es-le(es; e; e'), P  Q, es-dtype(es; i; x; T), x(s), decidable(P), es-locl(es; e; e'), A, False, wellfounded{i:l}(A; x,y.R(x;y))

Lemmas

es-when wf, es-vartype wf, es-loc wf, es-after wf, es-E wf, es-dtype wf, decidable wf, Id wf, event system wf, not wf, es-le wf, decidable l exists, es-interval wf2, decidable not, member-es-interval, l member subtype, Id sq, es-le-loc, squash wf, true wf, es-locl-wellfnd, l exists wf, es-locl wf, decidable assert, es-first wf, es-locl-iff, es-pred wf, es-pred-locl, es-le-pred, es-loc-pred, l member wf, strong-subtype-l member, strong-subtype-set3, strong-subtype-self